Termination Proof Script

Consider the TRS R consisting of the rewrite rules


1:		app(app(rec,h),app(g,0))	→ g
2:		app(app(rec,h),app(g,app(s,x)))	→ app(app(h,x),app(app(rec,h),app(g,x)))

There are 4 dependency pairs:


3:		APP(app(rec,h),app(g,app(s,x)))	→ APP(app(h,x),app(app(rec,h),app(g,x)))
4:		APP(app(rec,h),app(g,app(s,x)))	→ APP(h,x)
5:		APP(app(rec,h),app(g,app(s,x)))	→ APP(app(rec,h),app(g,x))
6:		APP(app(rec,h),app(g,app(s,x)))	→ APP(g,x)

Consider the SCC {3-6}. The constraints could not be solved.

Tyrolean Termination Tool (0.02 seconds) --- May 4, 2006